E,X1,X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), pred?:(E(?E)),
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(e:E, l:IdLnk.
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(e':E
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:((e'':E. 
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:((rcv?(e''))
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (sender(e'') = e)
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (link(e'') = l)
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (((e'' = e')  e'' < e')
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(  (loc(e') = destination(l)  Id)))),
e:E, l:IdLnk.
SWellFounded(pred!(e;e'))
 (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 (e,e':E. (loc(e) = loc(e')  Id)  (pred?(e) = pred?(e'))  (e = e'))
 (r:E. 
 (r  receives(dE; dL; pred?; info; p; e; l))
  ((rcv?(r)) c ((sender(r) = e)  (link(r) = l)))) 

latex

Definitions

False, x f y, rel_star(T; R), eventlist(pred?; e), sends-bound(p; e; l), P  Q, (x  l), receives(dE; dL; pred?; info; p; e; l), subtype(S; T), rcv-from-on(dE; dL; info; e; l; r), P  Q, , SWellFounded(R(x;y)), A c B, A, b, first(e), pred(e), x,y. t(x;y), pred!(e;e'), x:A. B(x), rcv?(e), sender(e), link(e), P  Q, P  Q, P  Q, e < e', prop{i:l}, loc(e), destination(l), Id, Unit, IdLnk, EqDecider(T), x:A. B(x), t  T

Lemmas

deq wf, IdLnk wf, unit wf, Id wf, ldst wf, loc wf, cless wf, link wf, sender wf, rcv? wf, assert wf, pred! wf, strongwellfounded wf, pred wf, first wf, not wf, nat wf, rcv-from-on wf, receives wf, l member wf, sends-bound wf, eventlist wf, member filter, assert-rcv-from-on, member eventlist, rel star wf, strong-sends-bound-property